{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module SemanticAnalyzer where

import Absclafer2alloy
import Common
import AlloyCode
import TypeEngine
import Monad
import List
import Data.Tree
import Data.Maybe
import Control.Monad.State
import Data.Map (Map)
import qualified Data.Map as Map

-- -----------------------------------------------------------------------------
-- environment used for dependencies: clafer, all clafers, predecessors, local bindings, symboltable
data SEnv = SEnv {
  clafer :: Maybe Clafer,
  declarations :: [Clafer],
  predecessors :: [Ident],
  bindings :: [Ident],
  st :: SymbolTable
  } deriving Show


getClafer (SEnv c _ _ _ _) = fromJust c


-- analyzes module by sorting and analyzing abstract clafers first, and then the
-- rest (clafers and constraints)
analyzeModule :: Module -> SymbolTable -> Module
analyzeModule x st = case x of
  Module declarations  -> Module $ multiProcess
    (map (\f -> 
        \ps us -> f (SEnv Nothing (mapMaybe toClafer $ ps ++ us) [] [] st)
                    (head us))
    [analyzeDeclaration, analyzeAbsClafer]) $
    uncurry ((++).(partialSort getMaxDecl)) $ partition isAbstract declarations


-- analyzes abstract clafer without its elements
analyzeAbsClafer :: SEnv -> Declaration -> Declaration
analyzeAbsClafer (SEnv _ declarations _ _ st) x = case x of
  EnumDecl ident enumids  -> error "desugared"
  AbsClaferDecl gcard ident super attr elements  ->
    toAbsClafer $ getClafer $ analyzeInherited $
    SEnv (toClafer x) declarations [] [] st
  ClaferDecl clafer  -> x
  ConstDecl constraint  -> x


-- analyzes all declarations 
analyzeDeclaration :: SEnv -> Declaration -> Declaration
analyzeDeclaration env@(SEnv _ declarations [] _ st) x = case x of
  EnumDecl ident enumids  -> error "desugared"
  AbsClaferDecl gcard ident super attr elements  -> toAbsClafer $ getClafer $
    analyzeElements $ analyzeOthers $ SEnv (toClafer x) declarations [] [] st
  ClaferDecl clafer  ->
    ClaferDecl $ analyzeClafer $ SEnv (Just clafer) declarations [] [] st
  ConstDecl constraint  -> ConstDecl $ analyzeConstraint env constraint


-- analyzes single clafer
analyzeClafer :: SEnv -> Clafer
analyzeClafer env =
  getClafer $ analyzeElements $ analyzeOthers $ analyzeInherited env


-- analyzes single constraint
analyzeConstraint :: SEnv -> Constraint -> Constraint
analyzeConstraint env x = case x of
  Constraint essential lexps  ->
    Constraint essential $ map (analyzeLExp env) lexps


-- analyzes inherited stuff (gcard and attribute)
analyzeInherited :: SEnv -> SEnv
analyzeInherited env@(SEnv (Just
  clafer@(Clafer gcard ident super attr essential card elements))
  declarations predecessors bindings st) =
    SEnv (Just $ Clafer (analyzeGCard gcard') ident super attr' essential card
      elements) declarations predecessors bindings st
  where
  hierarchy = findHierarchy declarations clafer
  gcard'    = findInList GCardEmpty (/= GCardEmpty) $ map getGCard hierarchy
  attrs     = filter (/= AttrEmpty) $ map getAttr $ tail hierarchy
  attr'     = case attr of
    AttrEmpty -> attr
    _         -> if null attrs then attr else toAttrSuper attr


-- analyzes attribute and adds itself to predecessors
analyzeOthers :: SEnv -> SEnv
analyzeOthers
  env@(SEnv (Just (Clafer gcard ident super attr essential card elements))
  declarations predecessors bindings st) =
    SEnv (Just $ Clafer gcard ident super (analyzeAttr env) essential card
       elements) declarations (ident : predecessors) bindings st


-- analyzes elements of a clafer
analyzeElements :: SEnv -> SEnv
analyzeElements
  env@(SEnv (Just (Clafer gcard ident super attr essential card elements))
  declarations predecessors bindings st) =
    SEnv (Just $ Clafer gcard ident super attr essential card
      (analyzeElements' env elements)) declarations predecessors bindings st


-- analyzes subclafers and constraints
analyzeElements' :: SEnv -> Elements -> Elements
analyzeElements' env x = case x of
  ElementsEmpty  -> error "desugared"
  Elements elements  -> Elements $ map (analyzeElement env) elements


-- analyzes subclafer or constraint
analyzeElement :: SEnv -> Element -> Element
analyzeElement env@(SEnv _ declarations predecessors bindings st) x = case x of
  Subclafer clafer  ->
    Subclafer $ analyzeClafer $
      SEnv (Just clafer) declarations predecessors bindings st
  ClaferUse name essential card elements -> error "desugared"
  Subconstraint constraint  -> Subconstraint $ analyzeConstraint env constraint


-- -----------------------------------------------------------------------------
-- desugars group cardinality to numerical values
analyzeGCard :: GCard -> GCard
analyzeGCard x = case x of
  GCardEmpty  -> GCardInterval $ GNCard 0 ExIntegerAst
  GCardXor -> GCardInterval $ GNCard 1 $ ExIntegerNum 1
  GCardOr  -> GCardInterval $ GNCard 1 $ ExIntegerAst
  GCardMux -> GCardInterval $ GNCard 0 $ ExIntegerNum 1
  GCardOpt -> GCardInterval $ GNCard 0 $ ExIntegerAst
  GCardInterval ncard  -> x


-- analyzes navigation, indicating that it should not be treated as a value
analyzeAttr :: SEnv -> Attr
analyzeAttr env = case getAttr $ getClafer env of
  AttrEmpty -> AttrEmpty
  AttrSExp  modids sexp -> AttrSExp modids $ analyzeSExp env False sexp
  AttrSuper modids sexp -> AttrSExp modids $ analyzeSExp env False sexp



-- analyzes logical expressions
analyzeLExp :: SEnv -> LExp -> LExp
analyzeLExp env x = case x of
  EIff lexp0 iff lexp  -> EIff (ana lexp0) iff (ana lexp)
  EImplies lexp0 implies lexp  ->
    EImplies (ana lexp0) implies (ana lexp)
  EImpliesElse lexp0 implies lexp1 lexp  -> EImpliesElse (ana lexp0)
    implies (ana lexp1) (ana lexp)
  EOr lexp0 or lexp  -> EOr (ana lexp0) or (ana lexp)
  EXor lexp0 xor lexp  -> EXor (ana lexp0) xor (ana lexp)
  EAnd lexp0 and lexp  -> EAnd (ana lexp0) and (ana lexp)
  ENeg neg lexp  -> ENeg neg (ana lexp)
  ETerm term  -> ETerm $ analyzeTerm env term
  where
  ana = analyzeLExp env


-- analyzes terms
analyzeTerm :: SEnv -> Term -> Term
analyzeTerm env@(SEnv clafer declarations predecessors bindings st) x =
  case x of
    TermCmpExp cmpexp  -> TermCmpExp $ analyzeCmpExp env cmpexp
    TermSet sexp        -> error "desugared"
    TermQuantSet quant sexp -> TermQuantSet quant (analyzeSExp env False sexp)
    TermQuantDeclExp decls lexp -> TermQuantDeclExp
      decls' (analyzeLExp env' lexp)
      where
      (decls', env') = runState (mapM processDecl decls) env


processDecl decl = do
  env <- get
  modify (\e -> e { bindings = getIdents decl ++ bindings e })
  return $ analyzeDecl env decl


-- analyzes decl
analyzeDecl :: SEnv -> Decl -> Decl
analyzeDecl env x = case x of
  Decl exquant disj locids sexp -> Decl exquant disj locids $ analyzeSExp env False sexp


-- analyzes relations
analyzeCmpExp :: SEnv -> CmpExp -> CmpExp
analyzeCmpExp env x = case x of
  ELt exp0 exp  -> ELt (ana exp0) (ana exp)
  EGt exp0 exp  -> EGt (ana exp0) (ana exp)
  EREq exp0 exp -> EREq (analyzeExp env False exp0) (analyzeExp env False exp)
  EEq exp0 exp  -> EEq (ana exp0) (ana exp)
  ELte exp0 exp  -> ELte (ana exp0) (ana exp)
  EGte exp0 exp  -> EGte (ana exp0) (ana exp)
  ENeq exp0 exp  -> ENeq (ana exp0) (ana exp)
  ERNeq exp0 exp -> ERNeq (analyzeExp env False exp0) (analyzeExp env False exp)
  EIn exp0 exp   -> EIn (analyzeExp env False exp0) (analyzeExp env False exp)
  ENin exp0 exp  -> ENin (ana exp0) (ana exp)
  where
  ana = analyzeExp env True


-- analyzes expressions
analyzeExp :: SEnv -> Bool -> Exp -> Exp
analyzeExp env isVal x = case x of
  ESetExp  sexp -> ESetExp  $ analyzeSExp env isVal sexp
  ENumExp aexp -> x
  EStrExp strexp -> x

-- -----------------------------------------------------------------------------
-- resolves path of starting identifier
analyzeSExp :: SEnv -> Bool -> SExp -> SExp
analyzeSExp env isVal x = analyzeSExp' env $ addSuffixSExp (toIdents valAttr) $
  addPrefixSExp (resolvePath env (getSExpStart x)) x
  where
  valAttr = if isVal then [valField] else []

{-
 Type inference rules for SExps
  a+b ^(a, b)
  a&b ^(a, b)
  a:>b b
  a<:b a
  a.b  b
  this.b b
  a.@.b b
  id id
-}
analyzeSExp' :: SEnv -> SExp -> SExp
analyzeSExp' env x = case x of
  SExpUnion sexp0 sexp -> SExpUnion (ana sexp0) (ana sexp)
  SExpIntersection sexp0 sexp  -> SExpIntersection (ana sexp0) (ana sexp)
  SExpDomain sexp0 sexp  -> SExpDomain (ana sexp0) (ana sexp)
  SExpRange sexp0 sexp  -> SExpRange (ana sexp0) (ana sexp)
  SExpJoin sexp0 sexp  -> SExpJoin (ana sexp0) (ana sexp)
  SExpArrow sexp0 sexp  -> error "desugared"
  SExpRIdent ident res -> SExpRIdent (
    if ident `elem` toIdents [this, parent, children] ++ bindings env
    then ident else Ident $ "@" ++ transIdent ident) -- TODO: remove @
    res
  where
  ana = analyzeSExp' env

---------------------------------------------------------------------------
{- TODO: new name resolution
type DEnv = Maybe Clafer

analyzeSExp :: SEnv -> Bool -> SExp -> SExp
analyzeSExp env isVal x = evalState (analyzeSExp' x) (clafer env)
{-
 analyzeSExp' env $ addSuffixSExp (toIdents valAttr) $
  addPrefixSExp (resolvePath env (getSExpStart x)) x
  where
  valAttr = if isVal then [valField] else []
-}

analyzeSExp' x = case x of
  SExpUnion sexp0 sexp -> error "not implemented"
  SExpIntersection sexp0 sexp  -> error "not implemented"
  SExpDomain sexp0 sexp  -> error "not implemented"
  SExpRange sexp0 sexp  -> error "not implemented"
  SExpJoin sexp0 sexp  -> do s0 <- analyzeSExp' sexp0
                             s  <- analyzeSExp' sexp
                             return $ SExpJoin s0 s
  SExpArrow sexp0 sexp  -> error "desugared"
  SExpRIdent ident  -> do env <- get
                         let ident' = resolvePath env ident
                   -- update env with target clafer- follow all the ref chain
                         modify (\e -> e {}

-- follow all refs, if ref resolved, mark it somehow
updateEnv ident = do
-}
---------------------------------------------------------------------------

-- returns starting point
getSExpStart :: SExp -> Ident
getSExpStart x = case x of
  SExpUnion sexp0 sexp -> getSExpStart sexp0
  SExpIntersection sexp0 sexp  -> getSExpStart sexp0
  SExpDomain sexp0 sexp  -> getSExpStart sexp0
  SExpRange sexp0 sexp  -> getSExpStart sexp0
  SExpJoin sexp0 sexp  -> getSExpStart sexp0
  SExpArrow sexp0 sexp  -> error "desugared"
  SExpRIdent ident _ -> ident


-- creates and adds prefix to sexp
addPrefixSExp :: [Ident] -> SExp -> SExp
addPrefixSExp idents x = case x of
  SExpUnion sexp0 sexp -> SExpUnion (addPrefixSExp idents sexp0) sexp 
  SExpIntersection sexp0 sexp  -> SExpIntersection (addPrefixSExp idents sexp0) sexp 
  SExpDomain sexp0 sexp  -> SExpDomain (addPrefixSExp idents sexp0) sexp 
  SExpRange sexp0 sexp  -> SExpRange (addPrefixSExp idents sexp0) sexp
  SExpJoin (SExpRIdent _ _) sexp -> SExpJoin (insertSExp [] idents) sexp
  SExpJoin sexp0 sexp         -> SExpJoin (addPrefixSExp idents sexp0) sexp
  SExpArrow sexp0 sexp        -> error "arrow desugared"
  SExpRIdent _ _              -> insertSExp [] idents


-- creates sexp from identifiers and inserts between sexps
insertSExp :: [SExp] -> [Ident] -> SExp
insertSExp = ((foldl1 SExpJoin).).(flip ((flip (++)).(map (flip SExpRIdent False))))


-- creates and adds suffix to sexp
addSuffixSExp = flip (insertSExp.(:[]))


-- -----------------------------------------------------------------------------
-- resolves path: 1) check if special (this, parent, ...),
-- 2) search subclafers  3) search in top level clafers, 4) report error
resolvePath :: SEnv -> Ident -> [Ident]
resolvePath env ident =
  reverse $ fromJust $ foldr1 mplus $ map (\x -> x env ident)
  [resolveSpecial, resolveBind, resolveSubclafers, resolveTopLevel, resolveNone]


-- reports error if clafer not found
resolveNone _ ident = error $ transIdent ident ++ " not found"


-- checks if ident is one of special identifiers
resolveSpecial :: SEnv -> Ident -> Maybe [Ident]
resolveSpecial _ ident
  | ident' `elem` [this, strType, intType, parent, children] = Just [ident]
  | otherwise                                                = Nothing 
  where
  ident' = transIdent ident


-- checks if ident is bound locally
resolveBind :: SEnv -> Ident -> Maybe [Ident]
resolveBind (SEnv _ _ _ bindings _) ident =
  find (== ident) bindings >>= (Just.(:[]))


-- searches for a name in subclafers (BFS)
resolveSubclafers :: SEnv -> Ident -> Maybe [Ident]
resolveSubclafers env@(SEnv clafer declarations predecessors bindings st) ident = clafer >> (findUnique env ident $ tail $ bfs toNode
  [SEnv clafer declarations [] bindings st])


-- converts clafer to a node (required by BFS algorithm)
toNode :: SEnv -> ([Ident], [SEnv])
toNode env@(SEnv (Just clafer) declarations predecessors bindings st) =
  (hNames, map (\f -> SEnv (Just f) declarations hNames bindings st) clafers)
  where
  hNames  = getClaferId clafer : predecessors
  clafers = mapMaybe extractClafer $ concatMap fromElements $
            mapHierarchy getElements declarations clafer


-- searches for a feature starting from local root (BFS) and then continues with
-- other declarations
resolveTopLevel :: SEnv -> Ident -> Maybe [Ident]
resolveTopLevel env@(SEnv _ declarations predecessors bindings st) ident =
  case predecessors of
    [] -> resolvePath declarations
    _  -> foldr1 mplus $ map resolvePath $ pairToList $
          partition (isEqClaferId (last predecessors)) declarations
    where
    resolvePath xs = findUnique env' ident $ bfs toNode $
                     map (\x -> env' { clafer = Just x }) xs
    env' = env { predecessors = [] }

findUnique (SEnv _ _ predecessors _ st) x xs =
  case filter (((==) x).head) xs of
    []     -> Nothing   -- TODO: new name resolution
    [elem] -> Just elem -- [lookupSymName (elem ++ predecessors) st] 
    _      -> error $ "element is not unique : " ++ show x

-- -----------------------------------------------------------------------------
-- analyzes arithmetic expression
analyzeAExp :: SEnv -> AExp -> AExp
analyzeAExp env x = case x of
  EAdd aexp0 aexp -> x
  ESub aexp0 aexp -> x
  EMul aexp0 aexp -> x
  EUmn aexp       -> x
  ECSetExp sexp   -> ECSetExp $ analyzeSExp env False sexp
  EInt n -> x